(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
a__f(X, X) → a__f(a, b)
a__b → a
mark(f(X1, X2)) → a__f(mark(X1), X2)
mark(b) → a__b
mark(a) → a
a__f(X1, X2) → f(X1, X2)
a__b → b
Rewrite Strategy: FULL
(1) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.
(2) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
a__f(X, X) → a__f(a, b)
a__b → a
mark(f(X1, X2)) → a__f(mark(X1), X2)
mark(b) → a__b
mark(a) → a
a__f(X1, X2) → f(X1, X2)
a__b → b
S is empty.
Rewrite Strategy: FULL
(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.
(4) Obligation:
TRS:
Rules:
a__f(X, X) → a__f(a, b)
a__b → a
mark(f(X1, X2)) → a__f(mark(X1), X2)
mark(b) → a__b
mark(a) → a
a__f(X1, X2) → f(X1, X2)
a__b → b
Types:
a__f :: a:b:f → a:b:f → a:b:f
a :: a:b:f
b :: a:b:f
a__b :: a:b:f
mark :: a:b:f → a:b:f
f :: a:b:f → a:b:f → a:b:f
hole_a:b:f1_0 :: a:b:f
gen_a:b:f2_0 :: Nat → a:b:f
(5) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
a__f,
markThey will be analysed ascendingly in the following order:
a__f < mark
(6) Obligation:
TRS:
Rules:
a__f(
X,
X) →
a__f(
a,
b)
a__b →
amark(
f(
X1,
X2)) →
a__f(
mark(
X1),
X2)
mark(
b) →
a__bmark(
a) →
aa__f(
X1,
X2) →
f(
X1,
X2)
a__b →
bTypes:
a__f :: a:b:f → a:b:f → a:b:f
a :: a:b:f
b :: a:b:f
a__b :: a:b:f
mark :: a:b:f → a:b:f
f :: a:b:f → a:b:f → a:b:f
hole_a:b:f1_0 :: a:b:f
gen_a:b:f2_0 :: Nat → a:b:f
Generator Equations:
gen_a:b:f2_0(0) ⇔ a
gen_a:b:f2_0(+(x, 1)) ⇔ f(gen_a:b:f2_0(x), a)
The following defined symbols remain to be analysed:
a__f, mark
They will be analysed ascendingly in the following order:
a__f < mark
(7) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol a__f.
(8) Obligation:
TRS:
Rules:
a__f(
X,
X) →
a__f(
a,
b)
a__b →
amark(
f(
X1,
X2)) →
a__f(
mark(
X1),
X2)
mark(
b) →
a__bmark(
a) →
aa__f(
X1,
X2) →
f(
X1,
X2)
a__b →
bTypes:
a__f :: a:b:f → a:b:f → a:b:f
a :: a:b:f
b :: a:b:f
a__b :: a:b:f
mark :: a:b:f → a:b:f
f :: a:b:f → a:b:f → a:b:f
hole_a:b:f1_0 :: a:b:f
gen_a:b:f2_0 :: Nat → a:b:f
Generator Equations:
gen_a:b:f2_0(0) ⇔ a
gen_a:b:f2_0(+(x, 1)) ⇔ f(gen_a:b:f2_0(x), a)
The following defined symbols remain to be analysed:
mark
(9) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
mark(
gen_a:b:f2_0(
+(
1,
n25_0))) →
*3_0, rt ∈ Ω(n25
0)
Induction Base:
mark(gen_a:b:f2_0(+(1, 0)))
Induction Step:
mark(gen_a:b:f2_0(+(1, +(n25_0, 1)))) →RΩ(1)
a__f(mark(gen_a:b:f2_0(+(1, n25_0))), a) →IH
a__f(*3_0, a)
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(10) Complex Obligation (BEST)
(11) Obligation:
TRS:
Rules:
a__f(
X,
X) →
a__f(
a,
b)
a__b →
amark(
f(
X1,
X2)) →
a__f(
mark(
X1),
X2)
mark(
b) →
a__bmark(
a) →
aa__f(
X1,
X2) →
f(
X1,
X2)
a__b →
bTypes:
a__f :: a:b:f → a:b:f → a:b:f
a :: a:b:f
b :: a:b:f
a__b :: a:b:f
mark :: a:b:f → a:b:f
f :: a:b:f → a:b:f → a:b:f
hole_a:b:f1_0 :: a:b:f
gen_a:b:f2_0 :: Nat → a:b:f
Lemmas:
mark(gen_a:b:f2_0(+(1, n25_0))) → *3_0, rt ∈ Ω(n250)
Generator Equations:
gen_a:b:f2_0(0) ⇔ a
gen_a:b:f2_0(+(x, 1)) ⇔ f(gen_a:b:f2_0(x), a)
No more defined symbols left to analyse.
(12) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
mark(gen_a:b:f2_0(+(1, n25_0))) → *3_0, rt ∈ Ω(n250)
(13) BOUNDS(n^1, INF)
(14) Obligation:
TRS:
Rules:
a__f(
X,
X) →
a__f(
a,
b)
a__b →
amark(
f(
X1,
X2)) →
a__f(
mark(
X1),
X2)
mark(
b) →
a__bmark(
a) →
aa__f(
X1,
X2) →
f(
X1,
X2)
a__b →
bTypes:
a__f :: a:b:f → a:b:f → a:b:f
a :: a:b:f
b :: a:b:f
a__b :: a:b:f
mark :: a:b:f → a:b:f
f :: a:b:f → a:b:f → a:b:f
hole_a:b:f1_0 :: a:b:f
gen_a:b:f2_0 :: Nat → a:b:f
Lemmas:
mark(gen_a:b:f2_0(+(1, n25_0))) → *3_0, rt ∈ Ω(n250)
Generator Equations:
gen_a:b:f2_0(0) ⇔ a
gen_a:b:f2_0(+(x, 1)) ⇔ f(gen_a:b:f2_0(x), a)
No more defined symbols left to analyse.
(15) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
mark(gen_a:b:f2_0(+(1, n25_0))) → *3_0, rt ∈ Ω(n250)
(16) BOUNDS(n^1, INF)